COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDCONST S0 ε situation
C00005 ENDMK
C⊗;
declare INDCONST S0 ε situation;
declare INDCONST Robot Outside Table Box1 Box2 Door ε tower;
declare PREDCONST key(tower) [pre];
declare PREDCONST red(tower)[pre];
declare PREDCONST asgood(tower,tower,situation);
declare PREDCONST exists(tower,situation);
declare OPCONST name(tower) = SEXPR;

axiom movable:
	∀t1 t2 s.(movable(t1,t2,s) ≡
(t1 = Robot ∧ (¬on(Robot,Outside,s)∨∃t.(key t ∧ on(t,Door,s))) ∧ (t2 = Table
	∨ t2 = Box1 ∨ t2 = Box2 ∨ t2 = Door) ∨
	(t2 = Outside ∧ ∃t.(key t ∧ on(t,Door,s))))
∨ t2 = Robot ∧ ∀t4.¬on(t4,Robot,s) ∧
	∃t3.(on(Robot,t3,s) ∧ on(t1,t3,s) ∧ ∀t4.(on(t4,t3,s) ⊃ asgood(t1,t4,s)))
∨ on(Robot,t2,s) ∧ on(t1,Robot,s))

	∀t1 t2 s.(movable(t1,t2,s) ≡
(t1 = Robot ∧ (t2 = Box1 ∨ t2 = Box2 ∨ t2 = Door ∨ t2 = Table ∨ t2 = Outside)
	∧ (¬(t2 = Outside) ∨ ∃t.(key t ∧ on(t,Door,s))))
∨ (t2 = Robot ∧ ∀t4.¬on(t4,Robot,s) ∧
	∃t3.(on(Robot,t3,s) ∧ on(t1,t3,s)))
∨ (on(t1,Robot,s) ∧ on(Robot,t2,s)))
;;

axiom asgood:
	∀t1 t2 s.(asgood(t1,t2,s) ∧ asgood(t2,t1,s) ⊃ t1 = t2)
	∀t1 t2 t3 s.(on(t2,t1,s) ∧ on(t3,t1,s) ⊃
		asgood(t2,t3,s) ∨ asgood(t3,t2,s))
	∀t1 t2 t3 s.(asgood(t1,t2,s) ∧ asgood(t2,t3,s) ⊃ asgood(t1,t3,s))
	∀t1 t2 s.(on(t2,t1,s) ⊃ ∃t3.(on(t3,t1,s) ∧ ∀t4.(on(t4,t1,s) ⊃
		asgood(t3,t4,s))))
;;

axiom initial:
	exists(Robot,S0) ∧ exists(Outside,S0) ∧ exists(Door,S0) ∧
exists(Box1,S0) ∧ exists(Box2,S0) ∧ exists(Table,S0)

	∃t1 t2.(key t1 ∧ (t2 = Box1 ∨ t2 = Box2) ∧ on(t1,t2,S0)
		∧ ∀t3.(on(t3,t2,S0) ⊃ key t3 ∨ t3 = Robot))

	∃t1.(red t1 ∧ on(t1,Door,S0))

	∀t1.(on(t1,Door,S0) ⊃ red t1 ∨ t1 = Robot)

	∀t.(on(t,Table,S0) ⊃ t = Robot)

	∀t1 t2.(on(t1,Robot,S0) ∧ on(t2,Robot,S0) ⊃ t1 = t2)

	¬on(Robot,Outside,S0)
;;

axiom names:
	name(Box1) = 'Box1
	name(Box2) = 'Box2
	name(Door) = 'Door
	name(Robot)='Robot
	name(Table) = 'Table
	name(Outside) = 'Outside
;;